↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
subset_in_ga([], X) → subset_out_ga([], X)
subset_in_ga(.(X, Xs), Ys) → U1_ga(X, Xs, Ys, member_in_aa(X, Ys))
member_in_aa(X, .(X, X1)) → member_out_aa(X, .(X, X1))
member_in_aa(X, .(X1, Xs)) → U3_aa(X, X1, Xs, member_in_aa(X, Xs))
U3_aa(X, X1, Xs, member_out_aa(X, Xs)) → member_out_aa(X, .(X1, Xs))
U1_ga(X, Xs, Ys, member_out_aa(X, Ys)) → U2_ga(X, Xs, Ys, subset_in_ag(Xs, Ys))
subset_in_ag([], X) → subset_out_ag([], X)
subset_in_ag(.(X, Xs), Ys) → U1_ag(X, Xs, Ys, member_in_ag(X, Ys))
member_in_ag(X, .(X, X1)) → member_out_ag(X, .(X, X1))
member_in_ag(X, .(X1, Xs)) → U3_ag(X, X1, Xs, member_in_aa(X, Xs))
U3_ag(X, X1, Xs, member_out_aa(X, Xs)) → member_out_ag(X, .(X1, Xs))
U1_ag(X, Xs, Ys, member_out_ag(X, Ys)) → U2_ag(X, Xs, Ys, subset_in_ag(Xs, Ys))
U2_ag(X, Xs, Ys, subset_out_ag(Xs, Ys)) → subset_out_ag(.(X, Xs), Ys)
U2_ga(X, Xs, Ys, subset_out_ag(Xs, Ys)) → subset_out_ga(.(X, Xs), Ys)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PrologToPiTRSProof
subset_in_ga([], X) → subset_out_ga([], X)
subset_in_ga(.(X, Xs), Ys) → U1_ga(X, Xs, Ys, member_in_aa(X, Ys))
member_in_aa(X, .(X, X1)) → member_out_aa(X, .(X, X1))
member_in_aa(X, .(X1, Xs)) → U3_aa(X, X1, Xs, member_in_aa(X, Xs))
U3_aa(X, X1, Xs, member_out_aa(X, Xs)) → member_out_aa(X, .(X1, Xs))
U1_ga(X, Xs, Ys, member_out_aa(X, Ys)) → U2_ga(X, Xs, Ys, subset_in_ag(Xs, Ys))
subset_in_ag([], X) → subset_out_ag([], X)
subset_in_ag(.(X, Xs), Ys) → U1_ag(X, Xs, Ys, member_in_ag(X, Ys))
member_in_ag(X, .(X, X1)) → member_out_ag(X, .(X, X1))
member_in_ag(X, .(X1, Xs)) → U3_ag(X, X1, Xs, member_in_aa(X, Xs))
U3_ag(X, X1, Xs, member_out_aa(X, Xs)) → member_out_ag(X, .(X1, Xs))
U1_ag(X, Xs, Ys, member_out_ag(X, Ys)) → U2_ag(X, Xs, Ys, subset_in_ag(Xs, Ys))
U2_ag(X, Xs, Ys, subset_out_ag(Xs, Ys)) → subset_out_ag(.(X, Xs), Ys)
U2_ga(X, Xs, Ys, subset_out_ag(Xs, Ys)) → subset_out_ga(.(X, Xs), Ys)
SUBSET_IN_GA(.(X, Xs), Ys) → U1_GA(X, Xs, Ys, member_in_aa(X, Ys))
SUBSET_IN_GA(.(X, Xs), Ys) → MEMBER_IN_AA(X, Ys)
MEMBER_IN_AA(X, .(X1, Xs)) → U3_AA(X, X1, Xs, member_in_aa(X, Xs))
MEMBER_IN_AA(X, .(X1, Xs)) → MEMBER_IN_AA(X, Xs)
U1_GA(X, Xs, Ys, member_out_aa(X, Ys)) → U2_GA(X, Xs, Ys, subset_in_ag(Xs, Ys))
U1_GA(X, Xs, Ys, member_out_aa(X, Ys)) → SUBSET_IN_AG(Xs, Ys)
SUBSET_IN_AG(.(X, Xs), Ys) → U1_AG(X, Xs, Ys, member_in_ag(X, Ys))
SUBSET_IN_AG(.(X, Xs), Ys) → MEMBER_IN_AG(X, Ys)
MEMBER_IN_AG(X, .(X1, Xs)) → U3_AG(X, X1, Xs, member_in_aa(X, Xs))
MEMBER_IN_AG(X, .(X1, Xs)) → MEMBER_IN_AA(X, Xs)
U1_AG(X, Xs, Ys, member_out_ag(X, Ys)) → U2_AG(X, Xs, Ys, subset_in_ag(Xs, Ys))
U1_AG(X, Xs, Ys, member_out_ag(X, Ys)) → SUBSET_IN_AG(Xs, Ys)
subset_in_ga([], X) → subset_out_ga([], X)
subset_in_ga(.(X, Xs), Ys) → U1_ga(X, Xs, Ys, member_in_aa(X, Ys))
member_in_aa(X, .(X, X1)) → member_out_aa(X, .(X, X1))
member_in_aa(X, .(X1, Xs)) → U3_aa(X, X1, Xs, member_in_aa(X, Xs))
U3_aa(X, X1, Xs, member_out_aa(X, Xs)) → member_out_aa(X, .(X1, Xs))
U1_ga(X, Xs, Ys, member_out_aa(X, Ys)) → U2_ga(X, Xs, Ys, subset_in_ag(Xs, Ys))
subset_in_ag([], X) → subset_out_ag([], X)
subset_in_ag(.(X, Xs), Ys) → U1_ag(X, Xs, Ys, member_in_ag(X, Ys))
member_in_ag(X, .(X, X1)) → member_out_ag(X, .(X, X1))
member_in_ag(X, .(X1, Xs)) → U3_ag(X, X1, Xs, member_in_aa(X, Xs))
U3_ag(X, X1, Xs, member_out_aa(X, Xs)) → member_out_ag(X, .(X1, Xs))
U1_ag(X, Xs, Ys, member_out_ag(X, Ys)) → U2_ag(X, Xs, Ys, subset_in_ag(Xs, Ys))
U2_ag(X, Xs, Ys, subset_out_ag(Xs, Ys)) → subset_out_ag(.(X, Xs), Ys)
U2_ga(X, Xs, Ys, subset_out_ag(Xs, Ys)) → subset_out_ga(.(X, Xs), Ys)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ PrologToPiTRSProof
SUBSET_IN_GA(.(X, Xs), Ys) → U1_GA(X, Xs, Ys, member_in_aa(X, Ys))
SUBSET_IN_GA(.(X, Xs), Ys) → MEMBER_IN_AA(X, Ys)
MEMBER_IN_AA(X, .(X1, Xs)) → U3_AA(X, X1, Xs, member_in_aa(X, Xs))
MEMBER_IN_AA(X, .(X1, Xs)) → MEMBER_IN_AA(X, Xs)
U1_GA(X, Xs, Ys, member_out_aa(X, Ys)) → U2_GA(X, Xs, Ys, subset_in_ag(Xs, Ys))
U1_GA(X, Xs, Ys, member_out_aa(X, Ys)) → SUBSET_IN_AG(Xs, Ys)
SUBSET_IN_AG(.(X, Xs), Ys) → U1_AG(X, Xs, Ys, member_in_ag(X, Ys))
SUBSET_IN_AG(.(X, Xs), Ys) → MEMBER_IN_AG(X, Ys)
MEMBER_IN_AG(X, .(X1, Xs)) → U3_AG(X, X1, Xs, member_in_aa(X, Xs))
MEMBER_IN_AG(X, .(X1, Xs)) → MEMBER_IN_AA(X, Xs)
U1_AG(X, Xs, Ys, member_out_ag(X, Ys)) → U2_AG(X, Xs, Ys, subset_in_ag(Xs, Ys))
U1_AG(X, Xs, Ys, member_out_ag(X, Ys)) → SUBSET_IN_AG(Xs, Ys)
subset_in_ga([], X) → subset_out_ga([], X)
subset_in_ga(.(X, Xs), Ys) → U1_ga(X, Xs, Ys, member_in_aa(X, Ys))
member_in_aa(X, .(X, X1)) → member_out_aa(X, .(X, X1))
member_in_aa(X, .(X1, Xs)) → U3_aa(X, X1, Xs, member_in_aa(X, Xs))
U3_aa(X, X1, Xs, member_out_aa(X, Xs)) → member_out_aa(X, .(X1, Xs))
U1_ga(X, Xs, Ys, member_out_aa(X, Ys)) → U2_ga(X, Xs, Ys, subset_in_ag(Xs, Ys))
subset_in_ag([], X) → subset_out_ag([], X)
subset_in_ag(.(X, Xs), Ys) → U1_ag(X, Xs, Ys, member_in_ag(X, Ys))
member_in_ag(X, .(X, X1)) → member_out_ag(X, .(X, X1))
member_in_ag(X, .(X1, Xs)) → U3_ag(X, X1, Xs, member_in_aa(X, Xs))
U3_ag(X, X1, Xs, member_out_aa(X, Xs)) → member_out_ag(X, .(X1, Xs))
U1_ag(X, Xs, Ys, member_out_ag(X, Ys)) → U2_ag(X, Xs, Ys, subset_in_ag(Xs, Ys))
U2_ag(X, Xs, Ys, subset_out_ag(Xs, Ys)) → subset_out_ag(.(X, Xs), Ys)
U2_ga(X, Xs, Ys, subset_out_ag(Xs, Ys)) → subset_out_ga(.(X, Xs), Ys)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PrologToPiTRSProof
MEMBER_IN_AA(X, .(X1, Xs)) → MEMBER_IN_AA(X, Xs)
subset_in_ga([], X) → subset_out_ga([], X)
subset_in_ga(.(X, Xs), Ys) → U1_ga(X, Xs, Ys, member_in_aa(X, Ys))
member_in_aa(X, .(X, X1)) → member_out_aa(X, .(X, X1))
member_in_aa(X, .(X1, Xs)) → U3_aa(X, X1, Xs, member_in_aa(X, Xs))
U3_aa(X, X1, Xs, member_out_aa(X, Xs)) → member_out_aa(X, .(X1, Xs))
U1_ga(X, Xs, Ys, member_out_aa(X, Ys)) → U2_ga(X, Xs, Ys, subset_in_ag(Xs, Ys))
subset_in_ag([], X) → subset_out_ag([], X)
subset_in_ag(.(X, Xs), Ys) → U1_ag(X, Xs, Ys, member_in_ag(X, Ys))
member_in_ag(X, .(X, X1)) → member_out_ag(X, .(X, X1))
member_in_ag(X, .(X1, Xs)) → U3_ag(X, X1, Xs, member_in_aa(X, Xs))
U3_ag(X, X1, Xs, member_out_aa(X, Xs)) → member_out_ag(X, .(X1, Xs))
U1_ag(X, Xs, Ys, member_out_ag(X, Ys)) → U2_ag(X, Xs, Ys, subset_in_ag(Xs, Ys))
U2_ag(X, Xs, Ys, subset_out_ag(Xs, Ys)) → subset_out_ag(.(X, Xs), Ys)
U2_ga(X, Xs, Ys, subset_out_ag(Xs, Ys)) → subset_out_ga(.(X, Xs), Ys)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ PiDP
↳ PrologToPiTRSProof
MEMBER_IN_AA(X, .(X1, Xs)) → MEMBER_IN_AA(X, Xs)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ NonTerminationProof
↳ PiDP
↳ PrologToPiTRSProof
MEMBER_IN_AA → MEMBER_IN_AA
MEMBER_IN_AA → MEMBER_IN_AA
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PrologToPiTRSProof
SUBSET_IN_AG(.(X, Xs), Ys) → U1_AG(X, Xs, Ys, member_in_ag(X, Ys))
U1_AG(X, Xs, Ys, member_out_ag(X, Ys)) → SUBSET_IN_AG(Xs, Ys)
subset_in_ga([], X) → subset_out_ga([], X)
subset_in_ga(.(X, Xs), Ys) → U1_ga(X, Xs, Ys, member_in_aa(X, Ys))
member_in_aa(X, .(X, X1)) → member_out_aa(X, .(X, X1))
member_in_aa(X, .(X1, Xs)) → U3_aa(X, X1, Xs, member_in_aa(X, Xs))
U3_aa(X, X1, Xs, member_out_aa(X, Xs)) → member_out_aa(X, .(X1, Xs))
U1_ga(X, Xs, Ys, member_out_aa(X, Ys)) → U2_ga(X, Xs, Ys, subset_in_ag(Xs, Ys))
subset_in_ag([], X) → subset_out_ag([], X)
subset_in_ag(.(X, Xs), Ys) → U1_ag(X, Xs, Ys, member_in_ag(X, Ys))
member_in_ag(X, .(X, X1)) → member_out_ag(X, .(X, X1))
member_in_ag(X, .(X1, Xs)) → U3_ag(X, X1, Xs, member_in_aa(X, Xs))
U3_ag(X, X1, Xs, member_out_aa(X, Xs)) → member_out_ag(X, .(X1, Xs))
U1_ag(X, Xs, Ys, member_out_ag(X, Ys)) → U2_ag(X, Xs, Ys, subset_in_ag(Xs, Ys))
U2_ag(X, Xs, Ys, subset_out_ag(Xs, Ys)) → subset_out_ag(.(X, Xs), Ys)
U2_ga(X, Xs, Ys, subset_out_ag(Xs, Ys)) → subset_out_ga(.(X, Xs), Ys)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ PrologToPiTRSProof
SUBSET_IN_AG(.(X, Xs), Ys) → U1_AG(X, Xs, Ys, member_in_ag(X, Ys))
U1_AG(X, Xs, Ys, member_out_ag(X, Ys)) → SUBSET_IN_AG(Xs, Ys)
member_in_ag(X, .(X, X1)) → member_out_ag(X, .(X, X1))
member_in_ag(X, .(X1, Xs)) → U3_ag(X, X1, Xs, member_in_aa(X, Xs))
U3_ag(X, X1, Xs, member_out_aa(X, Xs)) → member_out_ag(X, .(X1, Xs))
member_in_aa(X, .(X, X1)) → member_out_aa(X, .(X, X1))
member_in_aa(X, .(X1, Xs)) → U3_aa(X, X1, Xs, member_in_aa(X, Xs))
U3_aa(X, X1, Xs, member_out_aa(X, Xs)) → member_out_aa(X, .(X1, Xs))
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Narrowing
↳ PrologToPiTRSProof
SUBSET_IN_AG(Ys) → U1_AG(Ys, member_in_ag(Ys))
U1_AG(Ys, member_out_ag) → SUBSET_IN_AG(Ys)
member_in_ag(.) → member_out_ag
member_in_ag(.) → U3_ag(member_in_aa)
U3_ag(member_out_aa(Xs)) → member_out_ag
member_in_aa → member_out_aa(.)
member_in_aa → U3_aa(member_in_aa)
U3_aa(member_out_aa(Xs)) → member_out_aa(.)
member_in_ag(x0)
U3_ag(x0)
member_in_aa
U3_aa(x0)
SUBSET_IN_AG(.) → U1_AG(., member_out_ag)
SUBSET_IN_AG(.) → U1_AG(., U3_ag(member_in_aa))
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Narrowing
↳ QDP
↳ UsableRulesProof
↳ PrologToPiTRSProof
SUBSET_IN_AG(.) → U1_AG(., member_out_ag)
U1_AG(Ys, member_out_ag) → SUBSET_IN_AG(Ys)
SUBSET_IN_AG(.) → U1_AG(., U3_ag(member_in_aa))
member_in_ag(.) → member_out_ag
member_in_ag(.) → U3_ag(member_in_aa)
U3_ag(member_out_aa(Xs)) → member_out_ag
member_in_aa → member_out_aa(.)
member_in_aa → U3_aa(member_in_aa)
U3_aa(member_out_aa(Xs)) → member_out_aa(.)
member_in_ag(x0)
U3_ag(x0)
member_in_aa
U3_aa(x0)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Narrowing
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ PrologToPiTRSProof
SUBSET_IN_AG(.) → U1_AG(., member_out_ag)
U1_AG(Ys, member_out_ag) → SUBSET_IN_AG(Ys)
SUBSET_IN_AG(.) → U1_AG(., U3_ag(member_in_aa))
member_in_aa → member_out_aa(.)
member_in_aa → U3_aa(member_in_aa)
U3_ag(member_out_aa(Xs)) → member_out_ag
U3_aa(member_out_aa(Xs)) → member_out_aa(.)
member_in_ag(x0)
U3_ag(x0)
member_in_aa
U3_aa(x0)
member_in_ag(x0)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Narrowing
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Instantiation
↳ PrologToPiTRSProof
SUBSET_IN_AG(.) → U1_AG(., member_out_ag)
U1_AG(Ys, member_out_ag) → SUBSET_IN_AG(Ys)
SUBSET_IN_AG(.) → U1_AG(., U3_ag(member_in_aa))
member_in_aa → member_out_aa(.)
member_in_aa → U3_aa(member_in_aa)
U3_ag(member_out_aa(Xs)) → member_out_ag
U3_aa(member_out_aa(Xs)) → member_out_aa(.)
U3_ag(x0)
member_in_aa
U3_aa(x0)
U1_AG(., member_out_ag) → SUBSET_IN_AG(.)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Narrowing
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Instantiation
↳ QDP
↳ NonTerminationProof
↳ PrologToPiTRSProof
SUBSET_IN_AG(.) → U1_AG(., member_out_ag)
U1_AG(., member_out_ag) → SUBSET_IN_AG(.)
SUBSET_IN_AG(.) → U1_AG(., U3_ag(member_in_aa))
member_in_aa → member_out_aa(.)
member_in_aa → U3_aa(member_in_aa)
U3_ag(member_out_aa(Xs)) → member_out_ag
U3_aa(member_out_aa(Xs)) → member_out_aa(.)
U3_ag(x0)
member_in_aa
U3_aa(x0)
SUBSET_IN_AG(.) → U1_AG(., member_out_ag)
U1_AG(., member_out_ag) → SUBSET_IN_AG(.)
SUBSET_IN_AG(.) → U1_AG(., U3_ag(member_in_aa))
member_in_aa → member_out_aa(.)
member_in_aa → U3_aa(member_in_aa)
U3_ag(member_out_aa(Xs)) → member_out_ag
U3_aa(member_out_aa(Xs)) → member_out_aa(.)
subset_in_ga([], X) → subset_out_ga([], X)
subset_in_ga(.(X, Xs), Ys) → U1_ga(X, Xs, Ys, member_in_aa(X, Ys))
member_in_aa(X, .(X, X1)) → member_out_aa(X, .(X, X1))
member_in_aa(X, .(X1, Xs)) → U3_aa(X, X1, Xs, member_in_aa(X, Xs))
U3_aa(X, X1, Xs, member_out_aa(X, Xs)) → member_out_aa(X, .(X1, Xs))
U1_ga(X, Xs, Ys, member_out_aa(X, Ys)) → U2_ga(X, Xs, Ys, subset_in_ag(Xs, Ys))
subset_in_ag([], X) → subset_out_ag([], X)
subset_in_ag(.(X, Xs), Ys) → U1_ag(X, Xs, Ys, member_in_ag(X, Ys))
member_in_ag(X, .(X, X1)) → member_out_ag(X, .(X, X1))
member_in_ag(X, .(X1, Xs)) → U3_ag(X, X1, Xs, member_in_aa(X, Xs))
U3_ag(X, X1, Xs, member_out_aa(X, Xs)) → member_out_ag(X, .(X1, Xs))
U1_ag(X, Xs, Ys, member_out_ag(X, Ys)) → U2_ag(X, Xs, Ys, subset_in_ag(Xs, Ys))
U2_ag(X, Xs, Ys, subset_out_ag(Xs, Ys)) → subset_out_ag(.(X, Xs), Ys)
U2_ga(X, Xs, Ys, subset_out_ag(Xs, Ys)) → subset_out_ga(.(X, Xs), Ys)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
subset_in_ga([], X) → subset_out_ga([], X)
subset_in_ga(.(X, Xs), Ys) → U1_ga(X, Xs, Ys, member_in_aa(X, Ys))
member_in_aa(X, .(X, X1)) → member_out_aa(X, .(X, X1))
member_in_aa(X, .(X1, Xs)) → U3_aa(X, X1, Xs, member_in_aa(X, Xs))
U3_aa(X, X1, Xs, member_out_aa(X, Xs)) → member_out_aa(X, .(X1, Xs))
U1_ga(X, Xs, Ys, member_out_aa(X, Ys)) → U2_ga(X, Xs, Ys, subset_in_ag(Xs, Ys))
subset_in_ag([], X) → subset_out_ag([], X)
subset_in_ag(.(X, Xs), Ys) → U1_ag(X, Xs, Ys, member_in_ag(X, Ys))
member_in_ag(X, .(X, X1)) → member_out_ag(X, .(X, X1))
member_in_ag(X, .(X1, Xs)) → U3_ag(X, X1, Xs, member_in_aa(X, Xs))
U3_ag(X, X1, Xs, member_out_aa(X, Xs)) → member_out_ag(X, .(X1, Xs))
U1_ag(X, Xs, Ys, member_out_ag(X, Ys)) → U2_ag(X, Xs, Ys, subset_in_ag(Xs, Ys))
U2_ag(X, Xs, Ys, subset_out_ag(Xs, Ys)) → subset_out_ag(.(X, Xs), Ys)
U2_ga(X, Xs, Ys, subset_out_ag(Xs, Ys)) → subset_out_ga(.(X, Xs), Ys)
SUBSET_IN_GA(.(X, Xs), Ys) → U1_GA(X, Xs, Ys, member_in_aa(X, Ys))
SUBSET_IN_GA(.(X, Xs), Ys) → MEMBER_IN_AA(X, Ys)
MEMBER_IN_AA(X, .(X1, Xs)) → U3_AA(X, X1, Xs, member_in_aa(X, Xs))
MEMBER_IN_AA(X, .(X1, Xs)) → MEMBER_IN_AA(X, Xs)
U1_GA(X, Xs, Ys, member_out_aa(X, Ys)) → U2_GA(X, Xs, Ys, subset_in_ag(Xs, Ys))
U1_GA(X, Xs, Ys, member_out_aa(X, Ys)) → SUBSET_IN_AG(Xs, Ys)
SUBSET_IN_AG(.(X, Xs), Ys) → U1_AG(X, Xs, Ys, member_in_ag(X, Ys))
SUBSET_IN_AG(.(X, Xs), Ys) → MEMBER_IN_AG(X, Ys)
MEMBER_IN_AG(X, .(X1, Xs)) → U3_AG(X, X1, Xs, member_in_aa(X, Xs))
MEMBER_IN_AG(X, .(X1, Xs)) → MEMBER_IN_AA(X, Xs)
U1_AG(X, Xs, Ys, member_out_ag(X, Ys)) → U2_AG(X, Xs, Ys, subset_in_ag(Xs, Ys))
U1_AG(X, Xs, Ys, member_out_ag(X, Ys)) → SUBSET_IN_AG(Xs, Ys)
subset_in_ga([], X) → subset_out_ga([], X)
subset_in_ga(.(X, Xs), Ys) → U1_ga(X, Xs, Ys, member_in_aa(X, Ys))
member_in_aa(X, .(X, X1)) → member_out_aa(X, .(X, X1))
member_in_aa(X, .(X1, Xs)) → U3_aa(X, X1, Xs, member_in_aa(X, Xs))
U3_aa(X, X1, Xs, member_out_aa(X, Xs)) → member_out_aa(X, .(X1, Xs))
U1_ga(X, Xs, Ys, member_out_aa(X, Ys)) → U2_ga(X, Xs, Ys, subset_in_ag(Xs, Ys))
subset_in_ag([], X) → subset_out_ag([], X)
subset_in_ag(.(X, Xs), Ys) → U1_ag(X, Xs, Ys, member_in_ag(X, Ys))
member_in_ag(X, .(X, X1)) → member_out_ag(X, .(X, X1))
member_in_ag(X, .(X1, Xs)) → U3_ag(X, X1, Xs, member_in_aa(X, Xs))
U3_ag(X, X1, Xs, member_out_aa(X, Xs)) → member_out_ag(X, .(X1, Xs))
U1_ag(X, Xs, Ys, member_out_ag(X, Ys)) → U2_ag(X, Xs, Ys, subset_in_ag(Xs, Ys))
U2_ag(X, Xs, Ys, subset_out_ag(Xs, Ys)) → subset_out_ag(.(X, Xs), Ys)
U2_ga(X, Xs, Ys, subset_out_ag(Xs, Ys)) → subset_out_ga(.(X, Xs), Ys)
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
SUBSET_IN_GA(.(X, Xs), Ys) → U1_GA(X, Xs, Ys, member_in_aa(X, Ys))
SUBSET_IN_GA(.(X, Xs), Ys) → MEMBER_IN_AA(X, Ys)
MEMBER_IN_AA(X, .(X1, Xs)) → U3_AA(X, X1, Xs, member_in_aa(X, Xs))
MEMBER_IN_AA(X, .(X1, Xs)) → MEMBER_IN_AA(X, Xs)
U1_GA(X, Xs, Ys, member_out_aa(X, Ys)) → U2_GA(X, Xs, Ys, subset_in_ag(Xs, Ys))
U1_GA(X, Xs, Ys, member_out_aa(X, Ys)) → SUBSET_IN_AG(Xs, Ys)
SUBSET_IN_AG(.(X, Xs), Ys) → U1_AG(X, Xs, Ys, member_in_ag(X, Ys))
SUBSET_IN_AG(.(X, Xs), Ys) → MEMBER_IN_AG(X, Ys)
MEMBER_IN_AG(X, .(X1, Xs)) → U3_AG(X, X1, Xs, member_in_aa(X, Xs))
MEMBER_IN_AG(X, .(X1, Xs)) → MEMBER_IN_AA(X, Xs)
U1_AG(X, Xs, Ys, member_out_ag(X, Ys)) → U2_AG(X, Xs, Ys, subset_in_ag(Xs, Ys))
U1_AG(X, Xs, Ys, member_out_ag(X, Ys)) → SUBSET_IN_AG(Xs, Ys)
subset_in_ga([], X) → subset_out_ga([], X)
subset_in_ga(.(X, Xs), Ys) → U1_ga(X, Xs, Ys, member_in_aa(X, Ys))
member_in_aa(X, .(X, X1)) → member_out_aa(X, .(X, X1))
member_in_aa(X, .(X1, Xs)) → U3_aa(X, X1, Xs, member_in_aa(X, Xs))
U3_aa(X, X1, Xs, member_out_aa(X, Xs)) → member_out_aa(X, .(X1, Xs))
U1_ga(X, Xs, Ys, member_out_aa(X, Ys)) → U2_ga(X, Xs, Ys, subset_in_ag(Xs, Ys))
subset_in_ag([], X) → subset_out_ag([], X)
subset_in_ag(.(X, Xs), Ys) → U1_ag(X, Xs, Ys, member_in_ag(X, Ys))
member_in_ag(X, .(X, X1)) → member_out_ag(X, .(X, X1))
member_in_ag(X, .(X1, Xs)) → U3_ag(X, X1, Xs, member_in_aa(X, Xs))
U3_ag(X, X1, Xs, member_out_aa(X, Xs)) → member_out_ag(X, .(X1, Xs))
U1_ag(X, Xs, Ys, member_out_ag(X, Ys)) → U2_ag(X, Xs, Ys, subset_in_ag(Xs, Ys))
U2_ag(X, Xs, Ys, subset_out_ag(Xs, Ys)) → subset_out_ag(.(X, Xs), Ys)
U2_ga(X, Xs, Ys, subset_out_ag(Xs, Ys)) → subset_out_ga(.(X, Xs), Ys)
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
MEMBER_IN_AA(X, .(X1, Xs)) → MEMBER_IN_AA(X, Xs)
subset_in_ga([], X) → subset_out_ga([], X)
subset_in_ga(.(X, Xs), Ys) → U1_ga(X, Xs, Ys, member_in_aa(X, Ys))
member_in_aa(X, .(X, X1)) → member_out_aa(X, .(X, X1))
member_in_aa(X, .(X1, Xs)) → U3_aa(X, X1, Xs, member_in_aa(X, Xs))
U3_aa(X, X1, Xs, member_out_aa(X, Xs)) → member_out_aa(X, .(X1, Xs))
U1_ga(X, Xs, Ys, member_out_aa(X, Ys)) → U2_ga(X, Xs, Ys, subset_in_ag(Xs, Ys))
subset_in_ag([], X) → subset_out_ag([], X)
subset_in_ag(.(X, Xs), Ys) → U1_ag(X, Xs, Ys, member_in_ag(X, Ys))
member_in_ag(X, .(X, X1)) → member_out_ag(X, .(X, X1))
member_in_ag(X, .(X1, Xs)) → U3_ag(X, X1, Xs, member_in_aa(X, Xs))
U3_ag(X, X1, Xs, member_out_aa(X, Xs)) → member_out_ag(X, .(X1, Xs))
U1_ag(X, Xs, Ys, member_out_ag(X, Ys)) → U2_ag(X, Xs, Ys, subset_in_ag(Xs, Ys))
U2_ag(X, Xs, Ys, subset_out_ag(Xs, Ys)) → subset_out_ag(.(X, Xs), Ys)
U2_ga(X, Xs, Ys, subset_out_ag(Xs, Ys)) → subset_out_ga(.(X, Xs), Ys)
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ PiDP
MEMBER_IN_AA(X, .(X1, Xs)) → MEMBER_IN_AA(X, Xs)
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ NonTerminationProof
↳ PiDP
MEMBER_IN_AA → MEMBER_IN_AA
MEMBER_IN_AA → MEMBER_IN_AA
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
SUBSET_IN_AG(.(X, Xs), Ys) → U1_AG(X, Xs, Ys, member_in_ag(X, Ys))
U1_AG(X, Xs, Ys, member_out_ag(X, Ys)) → SUBSET_IN_AG(Xs, Ys)
subset_in_ga([], X) → subset_out_ga([], X)
subset_in_ga(.(X, Xs), Ys) → U1_ga(X, Xs, Ys, member_in_aa(X, Ys))
member_in_aa(X, .(X, X1)) → member_out_aa(X, .(X, X1))
member_in_aa(X, .(X1, Xs)) → U3_aa(X, X1, Xs, member_in_aa(X, Xs))
U3_aa(X, X1, Xs, member_out_aa(X, Xs)) → member_out_aa(X, .(X1, Xs))
U1_ga(X, Xs, Ys, member_out_aa(X, Ys)) → U2_ga(X, Xs, Ys, subset_in_ag(Xs, Ys))
subset_in_ag([], X) → subset_out_ag([], X)
subset_in_ag(.(X, Xs), Ys) → U1_ag(X, Xs, Ys, member_in_ag(X, Ys))
member_in_ag(X, .(X, X1)) → member_out_ag(X, .(X, X1))
member_in_ag(X, .(X1, Xs)) → U3_ag(X, X1, Xs, member_in_aa(X, Xs))
U3_ag(X, X1, Xs, member_out_aa(X, Xs)) → member_out_ag(X, .(X1, Xs))
U1_ag(X, Xs, Ys, member_out_ag(X, Ys)) → U2_ag(X, Xs, Ys, subset_in_ag(Xs, Ys))
U2_ag(X, Xs, Ys, subset_out_ag(Xs, Ys)) → subset_out_ag(.(X, Xs), Ys)
U2_ga(X, Xs, Ys, subset_out_ag(Xs, Ys)) → subset_out_ga(.(X, Xs), Ys)
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
SUBSET_IN_AG(.(X, Xs), Ys) → U1_AG(X, Xs, Ys, member_in_ag(X, Ys))
U1_AG(X, Xs, Ys, member_out_ag(X, Ys)) → SUBSET_IN_AG(Xs, Ys)
member_in_ag(X, .(X, X1)) → member_out_ag(X, .(X, X1))
member_in_ag(X, .(X1, Xs)) → U3_ag(X, X1, Xs, member_in_aa(X, Xs))
U3_ag(X, X1, Xs, member_out_aa(X, Xs)) → member_out_ag(X, .(X1, Xs))
member_in_aa(X, .(X, X1)) → member_out_aa(X, .(X, X1))
member_in_aa(X, .(X1, Xs)) → U3_aa(X, X1, Xs, member_in_aa(X, Xs))
U3_aa(X, X1, Xs, member_out_aa(X, Xs)) → member_out_aa(X, .(X1, Xs))
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Narrowing
SUBSET_IN_AG(Ys) → U1_AG(Ys, member_in_ag(Ys))
U1_AG(Ys, member_out_ag(Ys)) → SUBSET_IN_AG(Ys)
member_in_ag(.) → member_out_ag(.)
member_in_ag(.) → U3_ag(member_in_aa)
U3_ag(member_out_aa(Xs)) → member_out_ag(.)
member_in_aa → member_out_aa(.)
member_in_aa → U3_aa(member_in_aa)
U3_aa(member_out_aa(Xs)) → member_out_aa(.)
member_in_ag(x0)
U3_ag(x0)
member_in_aa
U3_aa(x0)
SUBSET_IN_AG(.) → U1_AG(., member_out_ag(.))
SUBSET_IN_AG(.) → U1_AG(., U3_ag(member_in_aa))
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Narrowing
↳ QDP
↳ UsableRulesProof
SUBSET_IN_AG(.) → U1_AG(., member_out_ag(.))
SUBSET_IN_AG(.) → U1_AG(., U3_ag(member_in_aa))
U1_AG(Ys, member_out_ag(Ys)) → SUBSET_IN_AG(Ys)
member_in_ag(.) → member_out_ag(.)
member_in_ag(.) → U3_ag(member_in_aa)
U3_ag(member_out_aa(Xs)) → member_out_ag(.)
member_in_aa → member_out_aa(.)
member_in_aa → U3_aa(member_in_aa)
U3_aa(member_out_aa(Xs)) → member_out_aa(.)
member_in_ag(x0)
U3_ag(x0)
member_in_aa
U3_aa(x0)
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Narrowing
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
SUBSET_IN_AG(.) → U1_AG(., member_out_ag(.))
SUBSET_IN_AG(.) → U1_AG(., U3_ag(member_in_aa))
U1_AG(Ys, member_out_ag(Ys)) → SUBSET_IN_AG(Ys)
member_in_aa → member_out_aa(.)
member_in_aa → U3_aa(member_in_aa)
U3_ag(member_out_aa(Xs)) → member_out_ag(.)
U3_aa(member_out_aa(Xs)) → member_out_aa(.)
member_in_ag(x0)
U3_ag(x0)
member_in_aa
U3_aa(x0)
member_in_ag(x0)
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Narrowing
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Instantiation
SUBSET_IN_AG(.) → U1_AG(., member_out_ag(.))
SUBSET_IN_AG(.) → U1_AG(., U3_ag(member_in_aa))
U1_AG(Ys, member_out_ag(Ys)) → SUBSET_IN_AG(Ys)
member_in_aa → member_out_aa(.)
member_in_aa → U3_aa(member_in_aa)
U3_ag(member_out_aa(Xs)) → member_out_ag(.)
U3_aa(member_out_aa(Xs)) → member_out_aa(.)
U3_ag(x0)
member_in_aa
U3_aa(x0)
U1_AG(., member_out_ag(.)) → SUBSET_IN_AG(.)
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Narrowing
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Instantiation
↳ QDP
↳ NonTerminationProof
SUBSET_IN_AG(.) → U1_AG(., member_out_ag(.))
U1_AG(., member_out_ag(.)) → SUBSET_IN_AG(.)
SUBSET_IN_AG(.) → U1_AG(., U3_ag(member_in_aa))
member_in_aa → member_out_aa(.)
member_in_aa → U3_aa(member_in_aa)
U3_ag(member_out_aa(Xs)) → member_out_ag(.)
U3_aa(member_out_aa(Xs)) → member_out_aa(.)
U3_ag(x0)
member_in_aa
U3_aa(x0)
SUBSET_IN_AG(.) → U1_AG(., member_out_ag(.))
U1_AG(., member_out_ag(.)) → SUBSET_IN_AG(.)
SUBSET_IN_AG(.) → U1_AG(., U3_ag(member_in_aa))
member_in_aa → member_out_aa(.)
member_in_aa → U3_aa(member_in_aa)
U3_ag(member_out_aa(Xs)) → member_out_ag(.)
U3_aa(member_out_aa(Xs)) → member_out_aa(.)